﻿/************************************************************************
 * AIDE - Automata Identification Engine
 * Copyright (C) 2012-2013 Ali Khalili (khalili_DOT_ir_@SIGN_gmail_DOT_com)
 * **********************************************************************
 * This program is free software; you can redistribute it and/or modify it
 * under the terms of the GNU Lesser General Public License (LGPL) published 
 * by the Free Software Foundation; either version 2.1 of the License, or (at your
 * option) any later version. This program is distributed without any
 * warranty. See the GNU Lesser General Public License for more details. 
 * ***********************************************************************
 * File         :     AIDE\OnlineAlgo\NFMs\DHC.cs
 * Description  :     Direct Hypothesis Construction (DHC) algorithm for learning (deterministic) Mealy machines
 *                    [Based on "Active automata learning for real-life applications (2013)" by Maik Merten]
 * Change log   :     -5 Feb 2013: Initial version
 *                    -6 Feb 2013: change "Oracle_MAT_Ideal" to "IOracle"
 * To Do        :     -Add cache
 *                    -Optimize counterexample processing
 ************************************************************************/
using System;
using System.Collections.Generic;
using AIDE.Base;
using SMLib.Automata.Base;
using SMLib.Automata.MM;
using AIDE.Oracles.NFMs;

/// <summary>
/// Online learning algorithms for (deterministic and nondeterministic) mealy machines
/// </summary>
namespace AIDE.OnlineAlgo.NFMs
{
    /// <summary>
    /// Direct Hypothesis Construction (DHC) algorithm for learning (deterministic) Mealy machines.
    /// <remarks>Based on "Active automata learning for real-life applications (2013)" by Maik Merten</remarks>
    /// </summary>
    public class DHC: INFM_Learner
    {
        #region =-[ Internal Class ]=-
        class NodeWithAccessString : MealyMachine.Mealy_State
        {
            internal Word accessString = new Word();

            internal List<Word> outputs = new List<Word>();
            internal List<Word> inputs = new List<Word>();
            internal List<NodeWithAccessString> otherDest = new List<NodeWithAccessString>();
            
            /// <summary>
            /// Constructor
            /// </summary>
            /// <param name="ID"></param>
            public NodeWithAccessString(string ID)
                : base(ID)
            {
                //* Nothing!
            }

            internal void AddTransitionOutput(Word symb, Word output)
            {
                inputs.Add(symb);
                outputs.Add(output);
            }

            /// <summary>
            /// FinalizeComputation (add transitions when constructing the conjecture)
            /// </summary>
            internal void FinalizeComputation()
            {
                for (int i = 0; i < inputs.Count; i++)
                {
                    if (inputs[i].Length > 1) 
                        continue;
                    //* in the previous line, we can even break!

                    MealyMachine.Mealy_Transition tr = new MealyMachine.Mealy_Transition
                        (inputs[i][0], outputs[i][0]);
                    tr.SetDestination(otherDest[i]);
                    Transitions.Add(tr);
                }
            }
        }

        /// <summary>
        /// Mealy machine with additional method related to DHC algorithm
        /// </summary>
        class ExtendedMealyMachine : MealyMachine
        {
            public void RerouteAllTransitions(NodeWithAccessString currentState, NodeWithAccessString sibling)
            {
                foreach (NodeWithAccessString n in states)
                {
                    for (int i = 0; i < n.otherDest.Count; i++)
                    {
                        if (n.otherDest[i] == currentState)
                        {
                            n.otherDest[i] = sibling;
                        }
                    }
                }
            }

            public void Remove(NodeWithAccessString currentState)
            {
                int index = 0;
                foreach (Mealy_State n in states)
                {
                    if (n == currentState)
                    {
                        break;
                    }
                    else
                        index++;
                }
                states.RemoveAt(index);
            }
        }
        #endregion

        IOracle_MAT_MM oracle;
        List<Word> inputAlphabet;

        /// <summary>
        /// Constructor
        /// </summary>
        /// <param name="oracle">the MAT oracle</param>
        public DHC(IOracle_MAT_MM oracle)
        {
            this.oracle = oracle;
            inputAlphabet = new List<Word>();

            //* Initialy, the input alphabet is the same as oracle's -system's in fact- input alphabet
            foreach (ISymbol symb in oracle.InputAlphabet.AllSymbols())
                inputAlphabet.Add(new Word(symb));
        }

        /// <summary>
        /// Learn the (deterministic) Mealy machine given the oracle
        /// </summary>
        /// <returns>The learnt Mealy model </returns>
        public MealyMachine Learn()
        {
            LearningLog.LogStartLearning();

            do
            {
                //* Based on current input alphabet, do learning
                MealyMachine conjecture = DHCLearning();
                //* And make the conjecture ready to use
                foreach (NodeWithAccessString n in conjecture.GetStates())
                    n.FinalizeComputation();

                //* Ask equivalence Query
                LearningLog.LogStartEQ();
                Word counterExample = oracle.EquivalenceQ(conjecture);
                LearningLog.LogFinishEQ();

                //* If no counterexample
                if (counterExample == null)
                {
                    LearningLog.LogFinishLearning();
                    return conjecture;
                }

                //* Else, process counterexample
                int i = conjecture.Size;
                ProcessCounterExample(counterExample, conjecture);

                //* Check if there is a problem!
                //if (i == conjecture.Size)
                //    throw new Exception("Something went wrong!");
            } while (true);
        }

        /// <summary>
        /// Process the counterexample: Add a word to input alphabet
        /// </summary>
        /// <param name="counterExample">the found counterexample</param>
        /// <param name="conjecture">the buildt conjecture</param>
        private void ProcessCounterExample(Word counterExample, MealyMachine conjecture)
        {
            int i;
            /*
            Oracle_MAT_Ideal tempOracle = new Oracle_MAT_Ideal(conjecture);
            Word myOutput;

            LearningLog.LogStartMQ();
            myOutput = oracle.OutputTrace(counterExample);
            LearningLog.LogFinishMQ();
			*/
            NodeWithAccessString currentNode = (NodeWithAccessString)conjecture.InitialState;
            
            for (i = 0; i < counterExample.Length; i++)
            {
                if (i != 0)
                {
                    Word input1 = currentNode.accessString.Clone();
                    Word input2 = counterExample.Prefix(i);

                    Word mySuffix = counterExample.Suffix(counterExample.Length - i);

                    input1.AddWord(mySuffix);
                    input2.AddWord(mySuffix);
                    if (!input1.Equals(input2))
                    {
                        //* Check that this suffix can distinguishes the system and conjecture
                        LearningLog.LogStartMQ();
                        Word sysOutput = oracle.OutputTrace(input1);
                        LearningLog.LogFinishMQ();

                        LearningLog.LogStartMQ();
                        Word conjOutput = oracle.OutputTrace(input2);
                        LearningLog.LogFinishMQ();

                        if (!sysOutput.Suffix(mySuffix.Length).Equals(conjOutput.Suffix(mySuffix.Length)))
                        {
                            bool cont = false;
                            foreach (Word mm in inputAlphabet)
                            {
                                if (mm.Equals(mySuffix))
                                    throw new Exception("!");
                            }
                            if (!cont)
                            {
                                inputAlphabet.Add(mySuffix);
                                return;
                            }
                        }
                    }
                }

                //* i-th step of counterexample
                ISymbol symb = counterExample[i];

                //* Go one step in the conjecture
                for (int j = 0; j < currentNode.inputs.Count; j++)
                {
                    if (currentNode.inputs[j].GetSymByIndex(0).Equals(symb))
                    {
                        currentNode = currentNode.otherDest[j];
                        break;
                    }
                }
            }
        }

        /// <summary>
        /// Find (if possible) another state with the same signiture (i.e. with the same expected things to see)
        /// </summary>
        /// <param name="currentState">the current state</param>
        /// <param name="m">the mealy machine</param>
        /// <returns>the other state, if not exists: null</returns>
        private NodeWithAccessString findOtherStateWithSameSignature(NodeWithAccessString currentState, ExtendedMealyMachine m)
        {
            foreach (NodeWithAccessString n in m.GetStates())
            {
                if (currentState == n)
                    continue;

                //* This will never happen!
                if (currentState.inputs.Count != n.inputs.Count)
                    continue;

                bool eq = true;
                for (int i = 0; i < currentState.inputs.Count; i++)
                {
                    if (n.inputs[i].Equals(currentState.inputs[i])
                        && n.outputs[i].Equals(currentState.outputs[i]))
                        continue;
                    eq = false;
                    break;
                }
                if (eq)
                    return n;
            }
            return null;
        }

        /// <summary>
        /// Constructing the hypothesis
        /// [Based on Page.42 of the thesis]
        /// </summary>
        /// <returns>the learnt conjecture</returns>
        MealyMachine DHCLearning()
        {
            int StateNumber = 1;

            //2 Hypothesis hypo=new Hypothesis();
            ExtendedMealyMachine hypo = new ExtendedMealyMachine();
            hypo.InputAlphabet = oracle.InputAlphabet;
            NodeWithAccessString startingNode = new NodeWithAccessString("s0");
            startingNode.accessString = new Word();
            hypo.AddState(startingNode);

            //3 Queue worklist = new Queue();
            List<NodeWithAccessString> worklist = new List<NodeWithAccessString>();

            //4 worklist.enqueue(hypo.getStartState());
            worklist.Add((NodeWithAccessString)hypo.InitialState);

            //5
            //6 while(worklist.isNotEmpty()){
            while (worklist.Count != 0)
            {
                //7 States currentState = worklist.dequeue();
                NodeWithAccessString currentState = worklist[0];
                worklist.RemoveAt(0);

                //8 Sequence accessSeq = currentState.getAccessSequence( ) ;
                Word accessSeq = currentState.accessString;

                //9 for (Symbol sym in alphabet) {
                foreach (Word symb in inputAlphabet)
                {
                    //10 Query query = accessSeq.append(sym) ;
                    Word query = accessSeq.Clone();
                    query.AddWord(symb);

                    //11
                    //12 * Communicate with the target system, fetch output symbol
                    //13 Symbol output = doMembershipQuery(query);
                    LearningLog.LogStartMQ();
                    Word output = oracle.OutputTrace(query);
                    LearningLog.LogFinishMQ();

                    //14
                    //15 * set the transition output for the sym input−symbol
                    //16 * to the retrieved output symbol .
                    //17 currentState.setTransitionOutput(sym,output);
                    currentState.AddTransitionOutput(symb, output.Suffix(symb.Length));
                    //18 }
                }

                //19
                //20 States sibling = findOtherStateWithSameSignature(currentState);
                NodeWithAccessString sibling = findOtherStateWithSameSignature(currentState, hypo);

                //21 if(exists(sibling)){
                if (sibling != null)
                {
                    //22 * reroute all transitions to current States to sibling
                    //23 hypo.rerouteAllTransitions(currentState,sibling);
                    hypo.RerouteAllTransitions(currentState, sibling);
                    //24 hypo.remove(currentState);
                    hypo.Remove(currentState);
                }
                //25 } else {
                else
                {
                    //26 currentState.createSuccesorsForEveryTransition();
                    //27 for(States successor of currentState){
                    //28 worklist.enqueue(successor);
                    //29 }
                    for (int i = 0; i < currentState.inputs.Count; i++)
                    {
                        NodeWithAccessString node = new NodeWithAccessString("s" + StateNumber);
                        StateNumber++;
                        node.accessString = currentState.accessString.Clone();
                        node.accessString.AddWord(currentState.inputs[i]);
                        hypo.AddState(node);
                        currentState.otherDest.Add(node);
                        worklist.Add(node);
                    }
                }
                //30 }
                //31 }
            }
            //32

            //33 return hypo ;
            return hypo;
            //34 }
        }
    }
}
